
; Copyright (c) 2015 Microsoft Corporation


(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)

(set-option :pp.flat-assoc false)


(dbg-bool-flat-rewriter 
 (let ((a1 (and a b)))
 (let ((a2 (and a1 a1)))
 (let ((a3 (and a1 a2)))
 (let ((a4 (and a3 a2)))
 (let ((a5 (and a4 a3)))
 (let ((a6 (and a5 a4)))
 (let ((a7 (and a6 a1)))
 (let ((a8 (and a7 a6)))
 (let ((a9 (and a8 a7)))
 (let ((a10 (and a9 a8)))
 (let ((a11 (and a10 a9)))
 (let ((a12 (and a11 a10)))
 (let ((a13 (and a11 a11)))
 (let ((a14 (and a13 a12)))
 (let ((a15 (and a14 a13)))
 (let ((a16 (and a15 a14)))
 (let ((a17 (and a16 a15)))
 (let ((a18 (and a17 a16)))
 (let ((a19 (and a18 a17)))
 (let ((a20 (and a19 a18)))
 (let ((a21 (and a20 a19)))
 (let ((a22 (and a21 a20)))
 (let ((a23 (and a21 a21)))
 (let ((a24 (and a23 a22)))
 (let ((a25 (and a24 a23)))
 (let ((a26 (and a25 a24)))
 (let ((a27 (and a26 a25)))
 (let ((a28 (and a27 a26)))
 (let ((a29 (and a28 a27)))
 (let ((a30 (and a29 a28)))
 (let ((a31 (and a30 a29)))
 (let ((a32 (and a31 a30)))
 (let ((a33 (and a31 a31)))
 (let ((a34 (and a33 a32)))
 (let ((a35 (and a34 a33)))
 (let ((a36 (and a35 a34)))
 (let ((a37 (and a36 a35)))
 (let ((a38 (and a37 a37)))
 (let ((a39 (and a38 a38)))
 (let ((a40 (and a38 a39)))
 (let ((a41 (and a40 a40)))
 (let ((a42 (and a41 a41)))
 (let ((a43 (and a41 a42)))
 (let ((a44 (and a43 a43)))
 (let ((a45 (and a44 a44)))
 (let ((a46 (and a45 a45)))
 (let ((a47 (and a46 a41)))
 (let ((a48 (and a47 a47)))
 (let ((a49 (and a48 a48)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a60 (and a58 a59)))
 (let ((a61 (and a60 a60)))
 (let ((a62 (and a61 a61)))
 (let ((a63 (and a61 a62)))
 (let ((a64 (and a63 a63)))
 (let ((a65 (and a64 a64)))
 (let ((a66 (and a65 a65)))
 (let ((a67 (and a66 a61)))
 (let ((a68 (and a67 a67)))
 (let ((a69 (and a68 a68)))
 (let ((a1 (and a68 a69)))
 (let ((a2 (and a1 a1)))
 (let ((a3 (and a1 a2)))
 (let ((a4 (and a3 a3)))
 (let ((a5 (and a4 a4)))
 (let ((a6 (and a5 a5)))
 (let ((a7 (and a6 a1)))
 (let ((a8 (and a7 a7)))
 (let ((a9 (and a8 a8)))
 (let ((a10 (and a9 a9)))
 (let ((a11 (and a10 a10)))
 (let ((a12 (and a11 a11)))
 (let ((a13 (and a11 a12)))
 (let ((a14 (and a13 a13)))
 (let ((a15 (and a14 a14)))
 (let ((a16 (and a15 a15)))
 (let ((a17 (and a16 a11)))
 (let ((a18 (and a17 a17)))
 (let ((a19 (and a18 a18)))
 (let ((a20 (and a19 a18)))
 (let ((a21 (and a20 a20)))
 (let ((a22 (and a21 a21)))
 (let ((a23 (and a21 a22)))
 (let ((a24 (and a23 a23)))
 (let ((a25 (and a24 a24)))
 (let ((a26 (and a25 a25)))
 (let ((a27 (and a26 a21)))
 (let ((a28 (and a27 a27)))
 (let ((a29 (and a28 a28)))
 (let ((a30 (and a29 a28)))
 (let ((a31 (and a30 a30)))
 (let ((a32 (and a31 a31)))
 (let ((a33 (and a31 a32)))
 (let ((a34 (and a33 a33)))
 (let ((a35 (and a34 a34)))
 (let ((a36 (and a35 a35)))
 (let ((a37 (and a36 a31)))
 (let ((a38 (and a37 a37)))
 (let ((a39 (and a38 a38)))
 (let ((a40 (and a38 a39)))
 (let ((a41 (and a40 a40)))
 (let ((a42 (and a41 a41)))
 (let ((a43 (and a41 a42)))
 (let ((a44 (and a43 a43)))
 (let ((a45 (and a44 a44)))
 (let ((a46 (and a45 a45)))
 (let ((a47 (and a46 a41)))
 (let ((a48 (and a47 a47)))
 (let ((a49 (and a48 a48)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a60 (and a58 a59)))
 (let ((a61 (and a60 a60)))
 (let ((a62 (and a61 a61)))
 (let ((a63 (and a61 a62)))
 (let ((a64 (and a63 a63)))
 (let ((a65 (and a64 a64)))
 (let ((a66 (and a65 a65)))
 (let ((a67 (and a66 a61)))
 (let ((a68 (and a67 a67)))
 (let ((a69 (and a68 a68)))
 (let ((a1 (and a68 a69 c)))
 (let ((a2 (and a1 a1)))
 (let ((a3 (and a1 a2)))
 (let ((a4 (and a3 a3)))
 (let ((a5 (and a4 a4)))
 (let ((a6 (and a5 a5)))
 (let ((a7 (and a6 a1)))
 (let ((a8 (and a7 a7)))
 (let ((a9 (and a8 a8)))
 (let ((a10 (and a9 a9)))
 (let ((a11 (and a10 a10)))
 (let ((a12 (and a11 a11)))
 (let ((a13 (and a11 a12)))
 (let ((a14 (and a13 a13)))
 (let ((a15 (and a14 a14)))
 (let ((a16 (and a15 a15)))
 (let ((a17 (and a16 a11)))
 (let ((a18 (and a17 a17)))
 (let ((a19 (and a18 a18)))
 (let ((a20 (and a19 a18)))
 (let ((a21 (and a20 a20)))
 (let ((a22 (and a21 a21)))
 (let ((a23 (and a21 a22)))
 (let ((a24 (and a23 a23)))
 (let ((a25 (and a24 a24)))
 (let ((a26 (and a25 a25)))
 (let ((a27 (and a26 a21)))
 (let ((a28 (and a27 a27)))
 (let ((a29 (and a28 a28)))
 (let ((a30 (and a29 a28)))
 (let ((a31 (and a30 a30)))
 (let ((a32 (and a31 a31)))
 (let ((a33 (and a31 a32)))
 (let ((a34 (and a33 a33)))
 (let ((a35 (and a34 a34)))
 (let ((a36 (and a35 a35)))
 (let ((a37 (and a36 a31)))
 (let ((a38 (and a37 a37)))
 (let ((a39 (and a38 a38)))
 (let ((a40 (and a38 a39)))
 (let ((a41 (and a40 a40)))
 (let ((a42 (and a41 a41)))
 (let ((a43 (and a41 a42)))
 (let ((a44 (and a43 a43)))
 (let ((a45 (and a44 a44)))
 (let ((a46 (and a45 a45)))
 (let ((a47 (and a46 a41)))
 (let ((a48 (and a47 a47)))
 (let ((a49 (and a48 a48)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a60 (and a58 a59)))
 (let ((a61 (and a60 a60)))
 (let ((a62 (and a61 a61)))
 (let ((a63 (and a61 a62)))
 (let ((a64 (and a63 a63)))
 (let ((a65 (and a64 a64)))
 (let ((a66 (and a65 a65)))
 (let ((a67 (and a66 a61)))
 (let ((a68 (and a67 a67)))
 (let ((a69 (and a68 a68)))
 (let ((a1 (and a69 a69)))
 (let ((a2 (and a1 a1)))
 (let ((a3 (and a1 a2)))
 (let ((a4 (and a3 a3)))
 (let ((a5 (and a4 a4)))
 (let ((a6 (and a5 a5)))
 (let ((a7 (and a6 a1)))
 (let ((a8 (and a7 a7)))
 (let ((a9 (and a8 a8)))
 (let ((a10 (and a9 a9)))
 (let ((a11 (and a10 a10)))
 (let ((a12 (and a11 a11)))
 (let ((a13 (and a11 a12)))
 (let ((a14 (and a13 a13)))
 (let ((a15 (and a14 a14)))
 (let ((a16 (and a15 a15)))
 (let ((a17 (and a16 a11)))
 (let ((a18 (and a17 a17)))
 (let ((a19 (and a18 a18)))
 (let ((a20 (and a19 a18)))
 (let ((a21 (and a20 a20)))
 (let ((a22 (and a21 a21)))
 (let ((a23 (and a21 a22)))
 (let ((a24 (and a23 a23)))
 (let ((a25 (and a24 a24)))
 (let ((a26 (and a25 a25)))
 (let ((a27 (and a26 a21)))
 (let ((a28 (and a27 a27)))
 (let ((a29 (and a28 a28)))
 (let ((a30 (and a29 a28)))
 (let ((a31 (and a30 a30)))
 (let ((a32 (and a31 a31)))
 (let ((a33 (and a31 a32)))
 (let ((a34 (and a33 a33)))
 (let ((a35 (and a34 a34)))
 (let ((a36 (and a35 a35)))
 (let ((a37 (and a36 a31)))
 (let ((a38 (and a37 a37)))
 (let ((a39 (and a38 a38)))
 (let ((a40 (and a38 a39)))
 (let ((a41 (and a40 a40)))
 (let ((a42 (and a41 a41)))
 (let ((a43 (and a41 a42)))
 (let ((a44 (and a43 a43)))
 (let ((a45 (and a44 a44)))
 (let ((a46 (and a45 a45)))
 (let ((a47 (and a46 a41)))
 (let ((a48 (and a47 a47)))
 (let ((a49 (and a48 a48)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a60 (and a58 a59)))
 (let ((a61 (and a60 a60)))
 (let ((a62 (and a61 a61)))
 (let ((a63 (and a61 a62)))
 (let ((a64 (and a63 a63)))
 (let ((a65 (and a64 a64)))
 (let ((a66 (and a65 a65)))
 (let ((a67 (and a66 a61)))
 (let ((a68 (and a67 a67)))
 (let ((a69 (and a68 a68)))
 (let ((a1 (and a68 a69)))
 (let ((a2 (and a1 a1)))
 (let ((a3 (and a1 a2)))
 (let ((a4 (and a3 a3)))
 (let ((a5 (and a4 a4)))
 (let ((a6 (and a5 a5)))
 (let ((a7 (and a6 a1)))
 (let ((a8 (and a7 a7)))
 (let ((a9 (and a8 a8)))
 (let ((a10 (and a9 a9)))
 (let ((a11 (and a10 a10)))
 (let ((a12 (and a11 a11)))
 (let ((a13 (and a11 a12)))
 (let ((a14 (and a13 a13)))
 (let ((a15 (and a14 a14)))
 (let ((a16 (and a15 a15)))
 (let ((a17 (and a16 a11)))
 (let ((a18 (and a17 a17)))
 (let ((a19 (and a18 a18)))
 (let ((a20 (and a19 a18)))
 (let ((a21 (and a20 a20)))
 (let ((a22 (and a21 a21)))
 (let ((a23 (and a21 a22)))
 (let ((a24 (and a23 a23)))
 (let ((a25 (and a24 a24)))
 (let ((a26 (and a25 a25)))
 (let ((a27 (and a26 a21)))
 (let ((a28 (and a27 a27)))
 (let ((a29 (and a28 a28)))
 (let ((a30 (and a29 a28)))
 (let ((a31 (and a30 a30)))
 (let ((a32 (and a31 a31)))
 (let ((a33 (and a31 a32)))
 (let ((a34 (and a33 a33)))
 (let ((a35 (and a34 a34)))
 (let ((a36 (and a35 a35)))
 (let ((a37 (and a36 a31)))
 (let ((a38 (and a37 a37)))
 (let ((a39 (and a38 a38)))
 (let ((a40 (and a38 a39)))
 (let ((a41 (and a40 a40)))
 (let ((a42 (and a41 a41)))
 (let ((a43 (and a41 a42)))
 (let ((a44 (and a43 a43)))
 (let ((a45 (and a44 a44)))
 (let ((a46 (and a45 a45)))
 (let ((a47 (and a46 a41)))
 (let ((a48 (and a47 a47)))
 (let ((a49 (and a48 a48)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a60 (and a58 a59)))
 (let ((a61 (and a60 a60)))
 (let ((a62 (and a61 a61)))
 (let ((a63 (and a61 a62)))
 (let ((a64 (and a63 a63)))
 (let ((a65 (and a64 a64)))
 (let ((a66 (and a65 a65)))
 (let ((a67 (and a66 a61)))
 (let ((a68 (and a67 a67)))
 (let ((a69 (and a68 a68)))
 (let ((a1 (and a68 a69 c)))
 (let ((a2 (and a1 a1)))
 (let ((a3 (and a1 a2)))
 (let ((a4 (and a3 a3)))
 (let ((a5 (and a4 a4)))
 (let ((a6 (and a5 a5)))
 (let ((a7 (and a6 a1)))
 (let ((a8 (and a7 a7)))
 (let ((a9 (and a8 a8)))
 (let ((a10 (and a9 a9)))
 (let ((a11 (and a10 a10)))
 (let ((a12 (and a11 a11)))
 (let ((a13 (and a11 a12)))
 (let ((a14 (and a13 a13)))
 (let ((a15 (and a14 a14)))
 (let ((a16 (and a15 a15)))
 (let ((a17 (and a16 a11)))
 (let ((a18 (and a17 a17)))
 (let ((a19 (and a18 a18)))
 (let ((a20 (and a19 a18)))
 (let ((a21 (and a20 a20)))
 (let ((a22 (and a21 a21)))
 (let ((a23 (and a21 a22)))
 (let ((a24 (and a23 a23)))
 (let ((a25 (and a24 a24)))
 (let ((a26 (and a25 a25)))
 (let ((a27 (and a26 a21)))
 (let ((a28 (and a27 a27)))
 (let ((a29 (and a28 a28)))
 (let ((a30 (and a29 a28)))
 (let ((a31 (and a30 a30)))
 (let ((a32 (and a31 a31)))
 (let ((a33 (and a31 a32)))
 (let ((a34 (and a33 a33)))
 (let ((a35 (and a34 a34)))
 (let ((a36 (and a35 a35)))
 (let ((a37 (and a36 a31)))
 (let ((a38 (and a37 a37)))
 (let ((a39 (and a38 a38)))
 (let ((a40 (and a38 a39)))
 (let ((a41 (and a40 a40)))
 (let ((a42 (and a41 a41)))
 (let ((a43 (and a41 a42)))
 (let ((a44 (and a43 a43)))
 (let ((a45 (and a44 a44)))
 (let ((a46 (and a45 a45)))
 (let ((a47 (and a46 a41)))
 (let ((a48 (and a47 a47)))
 (let ((a49 (and a48 a48)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a50 (and a48 a49)))
 (let ((a51 (and a50 a50)))
 (let ((a52 (and a51 a51)))
 (let ((a53 (and a51 a52)))
 (let ((a54 (and a53 a53)))
 (let ((a55 (and a54 a54)))
 (let ((a56 (and a55 a55)))
 (let ((a57 (and a56 a51)))
 (let ((a58 (and a57 a57)))
 (let ((a59 (and a58 a58)))
 (let ((a60 (and a58 a59)))
 (let ((a61 (and a60 a60)))
 (let ((a62 (and a61 a61)))
 (let ((a63 (and a61 a62)))
 (let ((a64 (and a63 a63)))
 (let ((a65 (and a64 a64)))
 (let ((a66 (and a65 a65)))
 (let ((a67 (and a66 a61)))
 (let ((a68 (and a67 a67)))
 (let ((a69 (and a68 a68)))
   a69)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

